Nuprl Lemma : comb_for_wellfounded_wf
9,38
postcript
pdf
(
A
,
r
,
z
. WellFnd{i}(
A
;
x
,
y
.
r
(
x
,
y
)))
A
:Type{i}
(
A
A
{i})
(
True)
{i'}
latex
ProofTree
Definitions
,
t
T
,
x
:
A
.
B
(
x
)
,
T
Lemmas
true
wf
,
squash
wf
,
wellfounded
wf
origin
A,r,z. WellFnd{i}(A;x,y.r(x,y))) 
A:Type{i}
(AA
{i})(
True){i'}
A,r,z. WellFnd{i}(A;x,y.r(x,y))) A:Type{i}(AA{i})(True){i'}
T
x:A. B(x)T